COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the pigeon hole principle
C00003 00003	* using the inductive predicate `all' the theorem comes quickly
C00005 00004	the arithmetical pigeon hole principle: long proof
C00010 00005	the pigeon hole principle on lists
C00029 ENDMK
C⊗;
;the pigeon hole principle
(wipe-out)
(get-proofs mult)

(proof pigeonfacts)

;the arithmetical form of the pigeon hole principle

(axiom |∀f n.(∀m.m<n⊃1≤f(m))∧sum(λk.f(k),n)≤n⊃(∀m.m<n⊃1=f(k))|)
(label pigeonfact)

;the pigeon hole principle on lists

(axiom |∀setseq u.disjoint(setseq,length u)∧
                  (∀k.k<length u⊃1≤mult(u,setseq(k)))⊃
                  (∀k.k<length u⊃1=mult(u,setseq(k)))|)
(label pigeonlist)

(save-proof pigeon)
;* using the inductive predicate `all' the theorem comes quickly;
    (wipe-out)
    (get-proofs sums)
    (proof pigeonfact)

1.  (ue (a |λn.all(n,λk.1≤f(k))⊃n≤sum(λk.f(k),n)|) 
        proof_by_induction 
        (open all sum)  zeroleast 
        (use add_lesseq ue: ((n.n)(k.|f(n)|)(m.|sum(λk.f(k),n)|)) ))
    (label strictly_increasing)

2.  (ue (a |λn.all(n,λk.1≤f(k))∧sum(λk.f(k),n)=n⊃all(n,λk.1=f(k))|)
        proof_by_induction (open all sum) strictly_increasing
        (use add_one ue: ((k.|f(n)|)(n.n)(m.|sum(λk.f(k),n)|)) mode: always))
    ;∀N.ALL(N,λK.1≤F(K))∧SUM(λK.F(K),N)=N⊃ALL(N,λK.1=F(K))

;in more conventional notation:

3.  (rw * (use allfact ue: ((a.|λk.1≤f(k)|)(n.n)) mode: exact direction: reverse)
          (use allfact ue: ((a.|λk.1=f(k)|)(n.n)) mode: exact direction: reverse))
    ;∀N.(∀M.M<N⊃1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M))

;the arithmetical pigeon hole principle: long proof
    (wipe-out)
    (get-proofs sums)

    (proof pigeonfact)

1.  (assume |(∀m.m<n⊃1≤f(m))⊃n≤sum(λk.f(k),n)|)
    (label pf1)

2.  (assume |∀m.m<n'⊃1≤f(m)|)
    (label pf2)

3.  (derive |n≤sum(λk.f(k),n)|(pf1 pf2 transitivity_of_order successor1))
    (label pf3)

4.  (ue (m n) pf2 successor1)
    ;1≤F(N)
    (label pf4)

5.  (ue ((n.n)(k.|f(n)|)(m.|sum(λk.f(k),n)|)) add_lesseq (pf3 pf4))
    ;N'≤SUM(λK.F(K),N)+F(N)

6.  (ci pf2)
    ;(∀M.M<N'⊃1≤F(M))⊃N'≤SUM(λK.F(K),N)+F(N)

7.  (ci pf1)

8.  (ue (a |λn.(∀m.m<n⊃1≤f(m))⊃n≤sum(λk.f(k),n)|) proof_by_induction 
        (open sum)  zeroleast (use * mode: always))
    ;∀N.(∀M.M<N⊃1≤F(M))⊃N≤SUM(λK.F(K),N)
    (label strictly_increasing)


;other direction


9.  (assume |(∀m.m<n⊃1≤f(m))∧sum(λk.f(k),n)=n⊃(∀m.m<n⊃1=f(m))|)
    (label pfindhyp)

10. (assume |∀m.m<n'⊃1≤f(m)|)
    (label pf_assume)

11. (derive |∀m.m<n⊃1≤f(m)| (pf_assume transitivity_of_order successor1))
    (label pf10)

12. (derive |1≤f(n)| (pf_assume successor1))
    (label pf11)

13. (assume |sum(λk.f(k),n')=n'|)
    (label pf_assume)

14. (rw * (open sum))
    ;N'=SUM(λK.F(K),N)+F(N)
    (label pf12)

;the case of f(n)

15. (derive |n≤sum(λk.f(k),n)| (strictly_increasing pf10))
    (label pf13)

;use
;labels: ADD_ONE 
;(AXIOM |∀K N M.1≤K∧N'=M+K∧N≤M⊃1=K∧N=M|)

16. (ue ((k.|f(n)|)(n.n)(m.|sum(λk.f(k),n)|)) add_one 
      (pf11 pf12 pf13))
    ;1=F(N)∧N=SUM(λK.F(K),N)
    (label pf14)

;use the induction hypothesis

17. (derive |∀m.m<n⊃1=f(m)| (pfindhyp pf10 *))
    (label pf15)

18. (derive |N0=N⊃1=F(N0)| pf14)
    ;deps: (PF_ASSUME)

19. (trw |∀m.m<n'⊃1=f(m)| (use less_succ_lesseq mode: exact) 
       (open lesseq) (use normal mode: always) pf15 *)
    ;∀M.M<N'⊃1=F(M)
    ;deps: (PF_ASSUME PFINDHYP)

20. (ci pf_assume)
    ;(∀M.M<N'⊃1≤F(M))∧SUM(λK.F(K),N')=N'⊃(∀M.M<N'⊃1=F(M))
    ;deps: (PFINDHYP)

21. (ci pfindhyp)

22. (ue (a |λn.(∀m.m<n⊃1≤f(m))∧sum(λk.f(k),n)=n⊃(∀m.m<n⊃1=f(m))|)
             proof_by_induction *)
    ;∀N.(∀M.M<N⊃1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M))

23. (trw |∀F N.(∀M.M<N⊃1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M))| *)
    ;∀F N.((∀M.M<N⊃1≤F(M))∧SUM(λK.F(K),N)=N⊃(∀M.M<N⊃1=F(M)))

;the pigeon hole principle on lists
    (wipe-out)
    (get-proofs pigeon)

(proof pigeonlist)
1.  (assume |disjoint(setseq,length u)|)
    (label pl1)

;multiplicity less than length

2.  (ue ((u.u)(a.|un(setseq,length u)|)) length_mult)
    ;MULT(U,UN(SETSEQ,LENGTH U))≤LENGTH U
    (label pl2)

3.  (derive |sum(λm.mult(u,setseq(m)),length u)≤length u| 
            (mult_of_un_is_sum_mult pl1 pl2))
    (label pl3)

4.  (ue ((f.|λm.mult(u,setseq(m))|)(n.|length u|)) pigeonfact pl3 multfact)
    ;(∀M.M<LENGTH U⊃1≤MULT(U,SETSEQ(M)))⊃(∀M.M<LENGTH U⊃1=MULT(U,SETSEQ(K)))
    ;deps: (PL1)

;the pigeon hole principle on lists

5.  (ci pl1)
    ;DISJOINT(SETSEQ,LENGTH U)⊃
    ;((∀M.M<LENGTH U⊃1≤MULT(U,SETSEQ(M)))⊃(∀M.M<LENGTH U⊃1=MULT(U,SETSEQ(K))))